/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.transl;

import alloy.ast.Op;
import alloy.ast.Node;
import alloy.ast.Leaf;
import alloy.ast.LeafId;
import alloy.ast.VarCreator;
import alloy.ast.DeclIter;
import alloy.ast.VariableExpr;
import alloy.ast.ASTDepthFirstVisitor;
import alloy.ast.HasType;
import alloy.ast.SigmaExpr;
import alloy.type.RelationType;
import alloy.util.Dbg;
import alloy.util.Params;
import alloy.util.CreationInfo;
import java.util.*;

/**
 * Checks sanity of the AST from which we are about to translate.
 * Causes an assertion failure if a check fails.  It also provides some warnings,
 * such as about possibly incorrect assignment of {@link LeafId}s to leaves that
 * can prevent us from {@linkplain alloy.sharbool.TemplateDetectVisitor detecting sharing}
 * of identical ground subformulas.
 *
 * The following invariants are checked:
 * <ul>
 * <li>That the AST is a tree -- no cycles (we may not actually rely on this)</li>
 * <li>That every leaf {@link Leaf#getLeafId has} a {@link LeafId}</li>
 * <li>That all leaves with the same {@link LeafId} represent the same AST node type (i.e. same Java {@link Class})</li>
 * <li>That all {@linkplain HasType relation-valued} leaves with the same {@link LeafId} the same {@link RelationType}. </li>
 * <li>That atomization has been fully performed: no {@link alloy.ast.UnionType}s or {@link SigmaExpr}s are left.</li>
 * <li>That every quantified variable referenced at a {@linkplain VariableExpr leaf} has been defined in a {@link VarCreator}
 *     higher up in the tree.</li>
 * <li></li>
 * </ul>
 *
 * todo:
 *    check that {@link BasicType} objects are properly canonicalized -- warn if there are two different basic type objects
 *    with the same string name.
 */
public class TranslatableASTCheckVisitor extends ASTDepthFirstVisitor {
    /**
     * {@link Set} of {@link Node}s already seen -- used to check that
     * the AST is indeed a tree and has no cycles.
     */
    private Set _nodesSeen = new TreeSet();

    /** {@link LeafId}s of {@link Variable}s defined at this point. */
    private Set _definedLeafIds = new HashSet();

    /**
     * For each {@link LeafId}, save a representative leaf with that id
     * so we when we later see leaves with that id we can make sure
     * they're alike.
     */
    private Map /* LeafId->Leaf */ _leafId2rep = new HashMap();

    /**
     * Map from String of a leaf to a representative leaf.  This lets us check,
     * when two leaves have the same string, whether they have the same {@link LeafId}s
     * (this needn't always be true -- esp. for leaves named "this" -- but usually should be.)
     */
    private Map /* String->Leaf */ _string2leafRep = new HashMap();

    /**
     * {@link Map} from {@link LeafId} to the {@link VarCreator} where it was
     * defined
     */
    private Map /* LeafId->VarCreator */ _var2creator = new HashMap();

    /**
     * {@link LeafId}s of quantified variables whose declarations
     * we have already encountered.  We should only encounter the declaration
     * of any given quantified variable once during traversal.  The difference from
     * {@link #_definedLeafIds} is that it is cumulative -- leaf ids are not
     * removed from this set when the declaration goes out of scope.  So we use this set
     * to check that leafids are globally unique -- declared in only one {@link VarCreator}.
     */
    private Set /* of LeafId */ _seenVarDeclarations = new HashSet();

    /////////////
    // Methods //
    /////////////

    /**
     * Check that all {@link SigmaExpr}s were removed during {@link alloy.transform.atomize.AtomizationVisitor atomization}.
     */
	public void visit(SigmaExpr n_) {
	    System.out.println("Encountered SigmaExpr " + n_);
	    if (n_.getParent() != null) {
		System.out.println("in " + n_.getParent());
	    }
	    
	    throw new RuntimeException();
	}

    /**
     * Check various node invariants (see class comment).
     */
    public void visit(Node n_) {
	//         System.out.println(n_.fullString());
	//         if (n_ instanceof VarCreator) System.out.println(((VarCreator)n_).getLeafIdMap());
	
	
	Dbg.chk(n_ instanceof Op || _nodesSeen.add(n_), "duplicate node " + n_.nodeString() + " at " + n_.getLocation().toString() + ", " + n_.getClass().toString());
	
	//System.out.println("Checking " + n_.nodeString() + " " + n_.getClass().toString());
	
	if (n_ instanceof Leaf) {
	    LeafId leafId = ((Leaf)n_).getLeafId();
	    Dbg.chk(leafId != null,
		    "no id for leaf " + n_.nodeString() + " at " + n_.getLocation().toString() + ", " +
		    n_.getClass().toString());
	    RelationType relType = null;
	    if (n_ instanceof HasType) {
		relType = ((HasType)n_).getType().toRelationType();
		Dbg.chk(relType, "node " + n_.nodeString() + 
			" has a non-atomized UnionType");
	    }

	    boolean isQuantVar = n_ instanceof VariableExpr &&
		((VariableExpr)n_).isQuantified;
	    if (isQuantVar) {
		Dbg.chk(_definedLeafIds.contains(leafId),
			"quantified variable " + n_ + " undefined");
		Dbg.chk(_var2creator.containsKey(leafId),
			"quantified variable " + n_ + " undefined");
	    }
	    
	    Leaf prior = (Leaf)_leafId2rep.get(leafId);
	    if (prior == null)
		_leafId2rep.put(leafId, n_);
	    else {
		String msg = null;
		RelationType priorType = (prior instanceof HasType) ? ((HasType)prior).getType().toRelationType() : null;
		boolean warnOnly = false;

		if (!n_.getClass().equals(prior.getClass()))
		    msg = "two leaves have same leaf ids but different classes";
		else if (relType != null && !relType.equals(priorType))
		    msg = "two leaves have same leaf ids but different relation types";
		else if (!n_.nodeString().equals(prior.nodeString()))
		    msg = "two leaves have same leaf ids but different nodeStrings";
			prior.nodeString();

		if (!Params.glob.getParam("DEVEL", "chkleaf", "ignore").equals("ignore")) {
		    String curString = n_.nodeString() + " (" + n_.getClass() + (relType!=null ? (" reltype " + relType) : "")+")";
		    if (isQuantVar)
			curString += " createdIn " + System.identityHashCode(_var2creator.get(leafId));
		    prior = (Leaf)_string2leafRep.get(curString);
		    if (prior== null)
			_string2leafRep.put(curString, n_);
		    else {
			if (!leafId.equals(prior.getLeafId())) {
			    msg = "two leaves have same nodeStrings, java classes and relation types but different leaf ids";
			    if (!Params.glob.getParam("DEVEL", "chkleaf", "ignore").equals("err"))
				warnOnly = true;
			}
		    }
		}
		
		if (msg != null) {
		    System.out.println("SANITY CHECK on translatable AST: " + msg);
		    _printLeafInfo("Leaf 1", prior);
		    _printLeafInfo("Leaf 2", (Leaf)n_);
		    if (!warnOnly)
			Dbg.chk(false, "Sanity check on translatable AST failed");
		}
	    }
	} else {
	    
	    Set /* of LeafId */ saveDefinedLeafIds = _definedLeafIds;
	    if (n_ instanceof VarCreator) {
		_definedLeafIds = new HashSet(_definedLeafIds);
		for (DeclIter declIter = new DeclIter((VarCreator)n_); declIter.hasNext();) {
		    declIter.next();
		    LeafId leafId = declIter.getLeafId();
		    Dbg.chk(leafId);
		    Dbg.chk(_definedLeafIds.add(leafId));
		    Dbg.chk(_seenVarDeclarations.add(leafId));
		    _var2creator.put(leafId, n_);
		}
	    }
            if (n_ instanceof HasType) {
                Dbg.chk(((HasType)n_).getType().toRelationType(), "node " + n_.nodeString() + 
			" has a non-atomized UnionType");
            }
 	    
	    /* Visit the children */
	    if (!(n_ instanceof Leaf)) {
		for (Iterator childIter = n_.getChildren(); childIter.hasNext();) {
		    Node child = (Node)childIter.next();
		    if (!(n_ instanceof VarCreator && child==((VarCreator)n_).getDecls())) {
			child.applyVisitor(this);
		    }
		}
	    }
	    
	    _definedLeafIds = saveDefinedLeafIds;
	}
    }

    /**
     * Print debugging information about a {@link Leaf}.
     */
    private static void _printLeafInfo(String msg_, Leaf leaf_) {
	System.out.println(msg_ + " - " + leaf_.nodeString());
	System.out.println("   leaf id " + leaf_.getLeafId() + " " +
			   leaf_.getClass() + (leaf_ instanceof HasType ? (" reltype " +
									   ((HasType)leaf_).getType().toRelationType()) : ""));
	System.out.println("   location in model: " + leaf_.getLocation());
	System.out.println("   creation info: " + CreationInfo.info(leaf_));
    }

    /**
     * @return <code>true</code> iff anc_ is an ancestor of node_.
     *         Note that a node is <em>not</em> its own ancestor.
     */
    /**
    private boolean _isAncestor(Node anc_, Node node_) {
 	Node parent = node_.getParent();
 	return parent!=null &&
 	    (parent == anc_ ||
 	     _isAncestor(anc_, parent));
    }

    **/
    
}
